Programación Avanzada

1 Contenido de la clase

Determinar precondiciones y poscondiciones en ternas de Hoare Pág. 82-83

Una terna de Hoare se escribe {P} C {Q}: P es la precondición, C el código y Q la poscondición. Para que sea correcta, si al ejecutar C se parte de un estado que cumple P, al terminar se debe cumplir Q.

Para calcular la precondición se sustituye en la poscondición el valor que adquiere la variable tras la asignación. Ejemplos de la conferencia:

• a) { P } j := i + 1 { j > 0 }. Como j pasa a valer i + 1, la precondición es { i + 1 > 0 } = { i > −1 }.
• b) { P } y := … { y > 1 }. Se sustituye la expresión asignada a y en la poscondición para obtener P.

Para calcular la poscondición se sustituye el valor de la variable (contenido en la precondición) en la asignación:

• c) { x > 2 } x := … { Q }. Como P = { x > 2 }, tras ejecutar la asignación la poscondición resulta { x > 4 }. Recordar que es sustituir en x := … el valor de x contenido en { P }.
• d) { P } x := … { x ≥ 0 }. La precondición queda { x > 0 } cuando x debe ser no nulo para que la expresión esté bien definida.

Qué interesa en la programación Pág. 84

Los ejemplos a), b) y d) muestran técnicas que se usarán más adelante para demostrar que un código es correcto. El ejemplo c) muestra lo que le interesa a la programación: dado un conjunto de datos iniciales y unas instrucciones, saber qué sigue después de ejecutarlas (saber qué hace el programa, cuál es el resultado).

Concatenación de código y su regla Pág. 84-85

La concatenación significa que las instrucciones se ejecutan secuencialmente: el estado final de la primera instrucción se convierte en el estado inicial de la segunda, y así sucesivamente.

Regla de la concatenación: si {P} C1 {R} y {R} C2 {Q} son correctas, entonces {P} C1; C2 {Q} es correcto.

Ejemplo (promedio): demostrar que es correcto { } c := a + b; c := c / 2 { c = (a + b) / 2 }. Se resuelve desde la última instrucción:

• Última instrucción: { P } c := c / 2 { c = (a + b) / 2 } → P = { c / 2 = (a + b) / 2 } = { c = a + b }. Así { c = a + b } c := c / 2 { c = (a + b) / 2 } … (1).
• Primera instrucción: { P } c := a + b { c = a + b } → P = { (a + b) = (a + b) } = { } (precondición vacía) … (2).
• Aplicando la regla de la concatenación a (1) y (2), el código es correcto.

Ejemplo (acumulador): { } s := 1; s := s + r; s := s + r × r { s = 1 + r + … }. La técnica es la misma: partir de la última instrucción, encontrar su precondición y encadenar hacia atrás.

Ejemplo (intercambio de valores): { a = A, b = B } h := a; a := b; b := h { a = B, b = A }. Trabajando desde el final:

• { P } b := h { a = B, b = A } → P = { a = B, h = A }.
• { P } a := b { a = B, h = A } → P = { b = B, h = A }.
• { P } h := a { h = A, b = B } → P = { a = A, b = B }.

Y aplicando la concatenación a las tres ternas, el código es correcto.

Invariante de un código Pág. 90-93

Cualquier aserción que es a la vez precondición y poscondición de un código se denomina invariante: el código no afecta a la aserción que se hace después de ejecutarlo; la relación entre variables se mantiene antes y después de ejecutar el código.

Ejemplo: demostrar que r = … (relación entre r e i) es un invariante de i := i + 1; r := r × 2; es decir, que es correcta la terna { r = … } i := i + 1; r := r × 2 { r = … }. Se encadenan con la regla de la concatenación las ternas de cada instrucción.

• Intuitivamente se comprueba con valores concretos: si i = 2 o i = 6, sustituyendo i y r se cumple la poscondición.
• Algebraicamente se sustituye el valor de i y de r y se comprueba que la relación se conserva.

Regla de inferencia de la sentencia if sin else Pág. 94-98

Si C1 es una parte de un programa y B una condición, la sentencia if B then C1 se interpreta: si B es verdadero se ejecuta C1. Para demostrar su corrección con {P} y {Q}:

• Si el estado inicial satisface B además de P, se ejecuta C1: demostrar que { P ∧ B } C1 { Q } es correcto.
• Si el estado inicial no satisface B: demostrar que { P ∧ ¬B } ⇒ { Q }.

{P ∧ B} C1 {Q} ; {P ∧ ¬B} ⇒ {Q} ⇒ {P} if B then C1 {Q}

Ejemplo: { } if (max < a) then max := a { max ≥ a }. Intuitivamente: si max < a → max := a { max = a }, que implica { max ≥ a }; si ¬(max < a) → max ≥ a. Formalmente se demuestran ambos casos (usando que { max < a } ⇒ { } y la regla de la asignación) y se aplica la regla del if.

Regla de inferencia de la sentencia if con else Pág. 99-100

Si C1 y C2 son dos partes de un programa y B una condición, la sentencia if B then C1 else C2 se interpreta: si B es verdadero se ejecuta C1; si no, C2. Las dos posibilidades de demostración son:

• Si el estado inicial satisface B además de P, se ejecuta C1: demostrar { P ∧ B } C1 { Q }.
• Si el estado inicial no satisface B, se ejecuta C2: demostrar { P ∧ ¬B } C2 { Q }.

{P ∧ B} C1 {Q} ; {P ∧ ¬B} C2 {Q} ⇒ {P} if B then C1 else C2 {Q}

2 Puntos destacados / Lo que hay que saber

3 Actividades y tareas pendientes

En esta clase (Nota 5) no se dejó una tarea nueva: la conferencia desarrolla ejemplos de cálculo de precondiciones/poscondiciones, la regla de la concatenación, el invariante y las reglas del if.

Queda pendiente de entregar la tarea de la clase anterior:

4 Dudas que podrían examinar

5 Sitios o recursos para visitar

El profesor no citó recursos web ni libros concretos en esta clase. Para profundizar en la verificación formal de programas se recomienda:

6 Glosario de términos

• Terna de Hoare: notación {P} C {Q} que relaciona precondición, código y poscondición.
• Precondición: aserción que debe cumplirse antes de ejecutar una instrucción o programa.
• Poscondición: aserción que se garantiza después de ejecutar una instrucción o programa.
• Aserción (assertion): predicado (relación entre variables) que describe el estado de un programa.
• Concatenación de código: ejecución secuencial de instrucciones; el estado final de una es el estado inicial de la siguiente.
• Regla de la concatenación: si {P} C1 {R} y {R} C2 {Q} son correctas, entonces {P} C1; C2 {Q} es correcto.
• Invariante de un código: aserción que es a la vez precondición y poscondición; el código no afecta a la relación entre variables.
• Regla de la asignación: al calcular precondiciones se sustituye en la poscondición el valor que toma la variable tras la asignación.
• Regla del if sin else: {P ∧ B} C1 {Q} y {P ∧ ¬B} ⇒ {Q} implican {P} if B then C1 {Q}.
• Regla del if con else: {P ∧ B} C1 {Q} y {P ∧ ¬B} C2 {Q} implican {P} if B then C1 else C2 {Q}.
• Precondición vacía ({ }): la aserción verdadera; no impone ninguna condición previa.

7 Mapa mental textual

• Programación Avanzada · Clase 5 · Verificación con la lógica de Hoare (Nota 5)
  • Ternas de Hoare {P} C {Q}
    • Calcular precondición: sustituir valor en la poscondición (ej. {P} j := i+1 {j>0} → {i>−1})
    • Calcular poscondición: sustituir x en {P} (ej. {x>2} x := … {Q} → {x>4})
    • Lo que interesa en programación: saber qué hace el programa
  • Concatenación y su regla
    • Estado final de una = estado inicial de la siguiente
    • Regla: {P} C1 {R}, {R} C2 {Q} ⇒ {P} C1; C2 {Q}
    • Ejemplos: promedio (c:=a+b; c:=c/2), acumulador (s:=1; s:=s+r; …), intercambio (h:=a; a:=b; b:=h)
    • Técnica: partir de la última instrucción y encadenar hacia atrás
  • Invariante de un código
    • Aserción que es precondición y poscondición a la vez
    • Ej.: relación r = … en i := i+1; r := r×2
    • Verificación intuitiva y algebraica
  • Reglas de inferencia de la sentencia if
    • Sin else: {P ∧ B} C1 {Q}, {P ∧ ¬B} ⇒ {Q} (ej. { } if (max<a) then max:=a {max≥a})
    • Con else: {P ∧ B} C1 {Q}, {P ∧ ¬B} C2 {Q}